ds:(IdType), da:(IdKndType), A:Type, X:Interface(ds;da;A), es:ES, e:E.
es-decl(es;ds;da)  (in-interface(es;X;e)  ) 

latex

Definitions	P  Q, , es-decl(es;ds;da), E, ES, x:A. B(x), Knd, x:AB(x), Id, t  T, Type, Interface(ds;da;A), in-interface(es;X;e), s = t, LocKnd, <a, b>, loc(e), kind(e), let x,y = A in B(x;y), t.1, x:A  B(x), x  dom(f), locknd-deq(), a:A fp B(a), x. t(x), x.A(x), let i,k:LocKnd = ik in P(i;k), x,y. t(x;y), f(a), left + right, Top, {x:A| B(x)} , b, hasloc(k;i)
Lemmas	hasloc wf, assert wf, top wf, locknd-spread wf2, fpf-trivial-subtype-top, locknd-deq wf, LocKnd wf, fpf-dom wf, es-hasloc, es-kind wf, es-loc wf, Id wf, Knd wf, interface wf, event system wf, es-E wf, es-decl wf